/*
 * SplittingTreeNode.hpp
 *
 * Copyright 2012 Fabian Wenzelmann
 *
 * This file is part of Recognition-Procedures-for-Boolean-Functions.
 *
 * Recognition-Procedures-for-Boolean-Functions is free software: you
 * can redistribute it and/or modify it under the terms of the
 * GNU General Public License as published by the Free Software Foundation,
 * either version 3 of the License, or (at your option) any later version.
 *
 * Recognition-Procedures-for-Boolean-Functions is distributed in the hope
 * that it will be useful, but WITHOUT ANY WARRANTY; without even the implied
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General
 * Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with Recognition-Procedures-for-Boolean-Functions.
 *
 * If not, see <http://www.gnu.org/licenses/>.
 */

#ifndef SPLITTINGTREENODE_HPP_
#define SPLITTINGTREENODE_HPP_

#include <utility>
#include <vector>

#include "bfr/lpbCombinatorial/TreeContext.hpp"
#include "bfr/ClauseSet.hpp"
#include "bfr/OccurrencePattern.hpp"
#include "bfr/NotSymmetricException.hpp"
#include "bfr/lpbCombinatorial/VariableSetting.hpp"
#include "bfr/lpbCombinatorial/SplitResult.hpp"

namespace bfr {

/**
 * Type of the Node.
 *
 * It is either a Main or an Auxiliary node.
 */
enum SplittingNodeType {
    MAIN_NODE, /*!< Main node type.*/
    AUXILIARY_NODE /*!< Aux node type.*/
};

struct MainNodeContent {
        // maximal l value. will be calculated automatically
        size_t maxL;
        // true if node is final
        bool final;
};

struct AuxNodeContent {
        // l
        size_t lValue;
        // l'
        size_t lPrime;
};

union SplittingNodeContent {
        MainNodeContent main;
        AuxNodeContent aux;
};

// TODO document special handling for main and aux exclusive fields

/**
 * Base class for nodes in a splitting tree.
 *
 * The algorithm proposed by
 * <a href="http://www.informatik.uni-freiburg.de/~ki/papers/smaus-tr230.pdf">
 * Smaus 2007
 * </a> <i>splits away</i> variables from DNFs to create subproblems. This
 * yields to a tree-like structure. We call this structure a
 * <i>Splitting Tree</i>.
 *
 * There are mainly two kinds of splitting tree nodes
 * <ul>
 *      <li>MainNode</li>
 *      <li>AuxiliaryNode</li>
 * </ul>
 *
 * MainNodes for the <i>main successors</i> of a DNF and
 * AuxiliaryNode for the <i>auxiliary successors</i> of
 * a DNF.
 *
 * Each node has an associated DNF \f$\phi\f$, pointers to child
 * and parent nodes.
 *
 * So each node has the following form:
 *
 * @image html st_node.png
 *
 * (image taken from my bachelor thesis
 * "Solving the Threshold Synthesis Problem of Boolean Functions by a
 * Combinatorial Algorithm", Wenzelmann 2011).
 */
class SplittingTreeNode {
    protected:
        /**
         * Pointer to the lower parent.
         */
        SplittingTreeNode *lowerParent;

        /**
         * Pointer to the upper parent.
         */
        SplittingTreeNode *upperParent;

        /**
         * Pointer to the lower child.
         */
        SplittingTreeNode *lowerChild;

        /**
         * Pointer to the upper child.
         */
        SplittingTreeNode *upperChild;

        /**
         * DNF \f$\phi\f$.
         */
        ClauseSet *dnf;

        /**
         * Global context of this node.
         */
        TreeContext *context;

        /**
         * Column of this node.
         */
        size_t column;

        /**
         * Row of this node.
         */
        size_t row;

        /**
         * The occurrence patterns for \f$\phi\f$.
         */
        std::vector<OccurrencePattern*> *occurrences;

        /**
         * The global variable setting.
         */
        // TODO: remove?!
        VariableSetting *setting;

        /**
         * Set to true if the split method has been called for this object.
         */
        bool alreadySplit;

        /**
         * Type of the node (either main or aux).
         */
        SplittingNodeType type;

    public:

        friend class SplittingTree;

        /**
         * The occurrence patterns for the dnf are stored in a vector.
         */
        typedef std::vector<OccurrencePattern*> pattern_container_t;

        // TODO: make methods protected, but I get some really strange errors
        /**
         * Set the lower parent of this node.
         */
        void setLowerParent(SplittingTreeNode *lp);

        /**
         * Set the upper parent of this node.
         */
        void setUpperParent(SplittingTreeNode *up);

        /**
         * Destructor.
         *
         * This method will destroy <b>only</b> the DNF and the occurrence
         * patterns. It will destroy neither the context, variable setting
         * nor child / parent objects.
         *
         * The DNF will <b>not</b> be destroyed if <code>column == 0</code>.
         * We assume that this functions was an argument to this function
         * and we don't have to care about it. All other DNFs however
         * are assumed to be internal objects.
         */
        ~SplittingTreeNode();

        /**
         * Constructor.
         *
         * Constructs a new splitting tree node given the parent nodes.
         *
         * <b>NOTE:</b> This method will <i>not</i> create the children
         * of this node by splitting away the next variable.
         * To achieve this create a SplittingTree and call
         * SplittingTree#createTree.
         *
         * The constructor will set the <code>column</code> value of the
         * node (by incrementing the <code>column</code> value of the
         * parent pointers by 1, if both parents are <code>NULL</code>
         * the value is set to 0).
         *
         * @param lp Pointer to the lower parent of the node.
         * @param up Pointer to the upper parent of the node.
         * @param d Pointer to the DNF \f$\phi\f$ of this node.
         * @param o pointer to a vector of the occurrence patterns for the DNF.
         * @param c The tree context, holds the whole tree in a vector.
         * @param t The type of this node.
         */
        SplittingTreeNode(SplittingTreeNode *lp, SplittingTreeNode *up,
                ClauseSet *d, std::vector<OccurrencePattern*> *o,
                TreeContext *c, SplittingNodeType t,
                const SplittingNodeContent &content);

        /**
         * The abstract split method (implemented differently in
         * MainNode and AuxiliaryNode class).
         *
         * The method must create the two successors of this node
         * (child nodes). You can use the methods #splitAway and #splitBoth
         * to create the DNFs / occurrence patterns, ...
         *
         * It must set the value of <code>alreadySplit</code>
         * to <code>true</code>.
         *
         * @param variables The global VariableSetting of all variables.
         * @param symmetryTest If this value is <code>true</code> a symmetry
         * test should be performed to check if the DNF fulfills the symmetry
         * property (see
         * <a href="http://www.informatik.uni-freiburg.de/~ki/papers/smaus-tr230.pdf">
         * Smaus 2007)
         * </a>.
         *
         * @throw NotSymmetricException If during the symmetry test a pair of
         * variables was found with identical occurrence patterns that are not
         * symmetric in \f$\phi\f$.
         */
        template<bool Cut>
        void split(VariableSetting *variables,
                bool symmetryTest=false) throw (NotSymmetricException) {
            if (type == SplittingNodeType::MAIN_NODE) {
	      //std::cout << "Splitting Main" << std::endl;
                splitMain<Cut>(variables, symmetryTest);
            }
            else {
	      //std::cout << "Splitting Aux" << std::endl;
                splitAux<Cut>(variables, symmetryTest);
            }
        }

        /**
         * Return <code>true</code> if this node is a <i>final node</i>.
         *
         * A node is called <i>final</i> if it is a MainNode and its DNF is
         * <i>true</i> or <i>false</i>.
         *
         * @return <code>true</code> if this node is a final node.
         */
        bool isFinal() const;

        /**
         * Return the lower parent of this node.
         *
         * @return The lower parent.
         */
        SplittingTreeNode *getLowerParent() const;

        /**
         * Return the upper parent of this node.
         *
         * @return The upper parent.
         */
        SplittingTreeNode *getUpperParent() const;

        /**
         * Return the lower child of this node.
         *
         * @return The lower child.
         */
        SplittingTreeNode *getLowerChild() const;

        /**
         * Return the upper child of this node.
         *
         * @return The upper child.
         */
        SplittingTreeNode *getUpperChild() const;

        /**
         * Return the DNF associated with this node.
         *
         * @return The DNF \f$\phi\f$.
         */
        ClauseSet *getDNF() const;

        /**
         * Return the column of this node.
         *
         * The columns are numbered starting with 0.
         *
         * @return The id of the column.in the tree.
         */
        size_t getColumn() const;

        /**
         * Return the row of this node.
         *
         * The rows are numbered starting with 0.
         *
         * @return The id of the row.in the tree.
         */
        size_t getRow() const;

        /**
         * Return the context of this node.
         *
         * @return The TreeContext that stores this node.
         */
        TreeContext *getContext() const;

        /**
         * Returns <code>true</code> if the #split method has already been
         * called for this node.
         *
         * @return <code>true</code> if split has already been called.
         */
        bool isAlreadySplit() const;

        /**
         * Split away the next variable.
         *
         * This methods splits away the most important variable
         * in the DNF (according to the occurrence patterns).
         *
         * The result is returned as a SplitResult, see the class
         * documentation there for the meaning.
         *
         * The variable to split away will be recognized from the
         * global variable setting.
         *
         * The value <code>k</code> should be either 0 or 1
         * (again see
         * <a href="http://www.informatik.uni-freiburg.de/~ki/papers/smaus-tr230.pdf">
         * Smaus 2007
         * </a>).
         *
         * If <code>k</code> is 0, the result contains a DNF that contains
         * all clauses from \f$\phi\f$ that do not contain the variable.
         *
         * If <code>k</code> is 1, the result contains a DNF that contains
         * all clauses from \f$\phi\f$ that contain the variable, but with
         * the variable removed.
         *
         * It also takes care of the \f$k_max\f$ value.
         *
         * If you have to create <b>both</b> successors of the DNF
         * (i. e. splitAway with <code>k</code> 0 and 1) use
         * #splitBoth which is more efficient than calling this
         * method for 0 and 1.
         *
         * BIG <b>TODO</b> The symmetryTest variable will be ignored,
         * no symmetry test is performed even the if the value is true.
         *
         * @param k Either 0 or 1, see text above.
         * @param variables The global variable information.
         * @param createPatterns If set to <code>true</code> the occurrences
         * for the new DNF will be calculated as well. Otherwise the
         * patterns are not create, i. e. set to NULL in the result.
         * @param symmetryTest If set to <code>true</code> this method will
         * perform a symmetry test. <b>TODO:</b> Actually we
         * ignore this variable.
         *
         * @throw NotSymmetricException If during the symmetry test a pair of
         * variables was found with identical occurrence patterns that are not
         * symmetric in \f$\phi\f$.
         *
         * @return The SplitResult when splitting away the most
         * important variable.
         */
        // BIG TODO
        // what if the clause is already present?
        // in this case I think it is wrong to use the occurrence we added!
        // can this happen somehow?
        SplitResult splitAway(short k,
                VariableSetting *variables,
                bool createPatterns=true,
                bool symmetryTest=true)
        throw (NotSymmetricException);

        /**
         * Split away 0 and 1 occurrences of the most important variable.
         *
         * This method is supposed to work exactly as #splitAway
         * but splits away 0 and 1 occurrences of the variable in one run.
         *
         * So the result returned by this method is equal to
         * \f$\langle splitAway(\phi, k=0),splitAway(\phi, k=1)\rangle\f$.
         *
         * @param variables The global variable information.
         * @param createPatterns If set to <code>true</code> the occurrences
         * for the new DNF will be calculated as well. Otherwise the
         * patterns are not create, i. e. set to NULL in the result.
         * @param symmetryTest If set to <code>true</code> this method will
         * perform a symmetry test. <b>TODO:</b> Actually we
         * ignore this variable.
         *
         * @throw NotSymmetricException If during the symmetry test a pair of
         * variables was found with identical occurrence patterns that are not
         * symmetric in \f$\phi\f$.
         *
         * @return The pair
         * \f$\langle splitAway(\phi, k=0),splitAway(\phi, k=1)\rangle\f$.
         *
         * @see splitAway
         */
        std::pair<SplitResult, SplitResult>
        splitBoth(VariableSetting *variables,
                bool createPatterns=true, bool symmetryTest=true)
                throw (NotSymmetricException);

        /**
         * Internal method to destroy the DNF and occurrence patterns.
         *
         * This method will destroy <b>only</b> the DNF and the occurrence
         * patterns. It will destroy neither the context, variable setting
         * nor child / parent objects.
         *
         * The DNF will <b>not</b> be destroyed if <code>column == 0</code>.
         * We assume that this functions was an argument to this function
         * and we don't have to care about it. All other DNFs however
         * are assumed to be internal objects.
         */
        void destroyContent(bool delFirstOccurrences=false);

    private:
        // private default constructor
        SplittingTreeNode();
        // private copy constructor
        SplittingTreeNode(const SplittingTreeNode &other);

    protected:
        // methods and fields for for main nodes

        // calculate if the node is a final node
        void calcIsFinal();
        // calculate the maximal l value
        size_t calcMaxL(VariableSetting *vs) const;

        template<bool Cut>
        void splitMain(VariableSetting *v,
                bool symmetryTest) {
            alreadySplit = true;

	    //std::cout << "will call calcMaxL(v)" << std::endl;
            // get maxL
            content.main.maxL = calcMaxL(v);
	    //std::cout << "content.main.maxL = " << content.main.maxL << std::endl;

            int nodeVal;
            if (Cut) {
                nodeVal = isDNFTrueOrFalse(*dnf);
            }

            if(content.main.maxL == 1) {
                if (Cut) {
                    if (nodeVal) {
                        if (nodeVal == 1) {
                            SplitResult result = splitAway(1, v, true, symmetryTest);
                            SplittingNodeContent newContent;
                            newContent.main.final = result.isFinal();
                            lowerChild = new SplittingTreeNode(0, this, result.getDNF(),
                                    result.getOccurrences(), context,
                                    MAIN_NODE, newContent);
                        }
                        else if (nodeVal == 2) {
                            SplitResult result = splitAway(0, v, true, symmetryTest);
                            SplittingNodeContent newContent;
                            newContent.main.final = result.isFinal();
                            upperChild = new SplittingTreeNode(this, 0, result.getDNF(),
                                    result.getOccurrences(), context,
                                    MAIN_NODE, newContent);
                        }
                        else {
                            assert(false);
                        }
                        return;
                    }
                }
                std::pair<SplitResult, SplitResult> res =
                        splitBoth(v, true, symmetryTest);
                SplitResult first = res.first;
                SplitResult second = res.second;
                SplittingNodeContent content1, content2;

                content1.main.final = first.isFinal();
                content2.main.final = second.isFinal();

                upperChild = new SplittingTreeNode(this, 0, first.getDNF(),
                        first.getOccurrences(), context, SplittingNodeType::MAIN_NODE,
                        content1);
                /*new MainNode(this, NULL, first.getDNF(),
                                                    first.getOccurrences(), context,
                                                    first.isFinal());*/
                lowerChild = new SplittingTreeNode(0, this, second.getDNF(),
                        second.getOccurrences(), context,
                        SplittingNodeType::MAIN_NODE, content2);
                /*new MainNode(NULL, this, second.getDNF(),
                                                    second.getOccurrences(), context,
                                                    second.isFinal());*/
            }
            else {
                if (Cut) {
                    if (nodeVal) {
                        SplittingNodeContent newContent;
                        newContent.aux.lPrime = 1;
                        newContent.aux.lValue = content.main.maxL;
                        if (nodeVal == 1) {
                            SplitResult result = splitAway(1, v, false, symmetryTest);
                            lowerChild = new SplittingTreeNode(0, this, result.getDNF(),
                                    result.getOccurrences(), context,
                                    AUXILIARY_NODE, newContent);
                        }
                        else if (nodeVal == 2) {
                            SplitResult result = splitAway(0, v, false, symmetryTest);
                            upperChild = new SplittingTreeNode(this, 0, result.getDNF(),
                                    result.getOccurrences(), context,
                                    AUXILIARY_NODE, newContent);
                        }
                        else {
                            assert(false);
                        }
                        return;
                    }
                }
                std::pair<SplitResult, SplitResult> res =
                        splitBoth(v, false, symmetryTest);
                SplitResult first = res.first;
                SplitResult second = res.second;

                SplittingNodeContent content1, content2;
                content1.aux.lValue = content.main.maxL;
                content1.aux.lPrime = 1;
                content2.aux.lValue = content.main.maxL;
                content2.aux.lPrime = 1;

                upperChild = new SplittingTreeNode(this, 0, first.getDNF(),
                        first.getOccurrences(), context, AUXILIARY_NODE,
                        content1);
                /*new AuxiliaryNode(this, NULL, first.getDNF(),
                                               first.getOccurrences(), context,
                                               maxL, 1);*/
                lowerChild = new SplittingTreeNode(0, this, second.getDNF(),
                        second.getOccurrences(), context, AUXILIARY_NODE,
                        content2);
                /*new AuxiliaryNode(NULL, this, second.getDNF(),
                                               second.getOccurrences(), context,
                                               maxL, 1);*/
            }
        }

        // end methods and fields for main nodes

        // methods and fields for aux nodes
        // check if a main node should be created
        bool createMainNode() const;

        template<bool Cut>
        void splitAux(VariableSetting *v,
                bool symmetryTest) {
            alreadySplit = true;
            bool createBoth = false;

            int nodeVal;

            if (Cut) {
                nodeVal = isDNFTrueOrFalse(*dnf);
                if (nodeVal) {
                    // std::cout << "at column " << column << " node " << this << std::endl;
                    // std::cout << "NODE VAL SET: " << nodeVal << " = " << *dnf << std::endl;
                    if (nodeVal == 1) {
                        // std::cout << "MainNode?: " << createMainNode() << std::endl;
                        SplittingNodeContent newContent;
                        if (createMainNode()) {
                            SplitResult result = splitAway(1, v, true, symmetryTest);
                            newContent.main.final = result.isFinal();
                            lowerChild = new SplittingTreeNode(0, this, result.getDNF(),
                                    result.getOccurrences(), context,
                                    MAIN_NODE, newContent);
                        } else {
                            SplitResult result = splitAway(1, v, false, symmetryTest);
                            newContent.aux.lValue = content.aux.lValue;
                            newContent.aux.lPrime = content.aux.lPrime + 1;
                            lowerChild = new SplittingTreeNode(0, this, result.getDNF(),
                                    result.getOccurrences(), context, AUXILIARY_NODE,
                                    newContent);
                        }
                    }
                    else if (nodeVal == 2) {                        
                        assert (upperParent->getUpperChild() != NULL);
                        upperChild = upperParent->getUpperChild()->getLowerChild();
                    }
                    else {
                        assert(false);
                    }
                    // std::cout << "DONE " << this->upperChild << " " << this->lowerChild << std::endl;
                    return;
                }
            }
            // std::cout << "no trivial case, DNF = " << *dnf << std::endl;

            if (upperParent != NULL) {
                assert (upperParent->getUpperChild() != NULL);
                upperChild = upperParent->getUpperChild()->getLowerChild();
                upperChild->setLowerParent(this);
            }
            else {
                createBoth = true;
            }

            if (createBoth) {

                if (createMainNode()) {
                    std::pair<SplitResult, SplitResult> splitResult =
                            splitBoth(v,
                                    true, symmetryTest);
                    SplitResult first = splitResult.first;
                    SplitResult second = splitResult.second;

                    SplittingNodeContent content1, content2;
                    content1.main.final = first.isFinal();
                    content2.main.final = second.isFinal();

                    upperChild = new SplittingTreeNode(this, 0, first.getDNF(),
                            first.getOccurrences(), context, SplittingNodeType::MAIN_NODE,
                            content1);
                    /*new MainNode(this, NULL, first.getDNF(),
                            first.getOccurrences(), context, first.isFinal());*/
                    lowerChild = new SplittingTreeNode(0, this, second.getDNF(),
                            second.getOccurrences(), context, SplittingNodeType::MAIN_NODE,
                            content2);
                    /*new MainNode(NULL, this, second.getDNF(),
                            second.getOccurrences(), context, second.isFinal());*/
                }
                else {
                    std::pair<SplitResult, SplitResult> splitResult =
                            splitBoth(v,
                                    false, symmetryTest);
                    SplitResult first = splitResult.first;
                    SplitResult second = splitResult.second;

                    SplittingNodeContent content1, content2;
                    content1.aux.lValue = content.aux.lValue;
                    content1.aux.lPrime = content.aux.lPrime + 1;
                    content2.aux.lValue = content.aux.lValue;
                    content2.aux.lPrime = content.aux.lPrime + 1;

                    upperChild = new SplittingTreeNode(this, 0, first.getDNF(),
                            first.getOccurrences(), context, SplittingNodeType::AUXILIARY_NODE,
                            content1);
                    /*new AuxiliaryNode(this, NULL, first.getDNF(),
                            first.getOccurrences(), context, lValue, lPrime + 1);*/
                    lowerChild = new SplittingTreeNode(0, this, second.getDNF(),
                            second.getOccurrences(), context, SplittingNodeType::AUXILIARY_NODE,
                            content2);
                    /*new AuxiliaryNode(NULL, this, second.getDNF(),
                            second.getOccurrences(), context, lValue, lPrime + 1);*/
                }
            }
            else {
                if (createMainNode()) {
                    SplitResult splitResult = splitAway(1, v,
                            true, symmetryTest);
                    lowerChild = new SplittingTreeNode(0, this, splitResult.getDNF(),
                            splitResult.getOccurrences(), context, SplittingNodeType::MAIN_NODE,
                            SplittingNodeContent());
                    // TODO: not happy with that...
                    lowerChild->calcIsFinal();
                    /*new MainNode(NULL, this, splitResult.getDNF(),
                                              splitResult.getOccurrences(), context);*/

                }
                else {
                    // TODO: why is create patterns set to false but we use them?!
                    SplitResult splitResult =
                            splitAway(1, v, false, symmetryTest);

                    SplittingNodeContent childContent;
                    childContent.aux.lValue = content.aux.lValue;
                    childContent.aux.lPrime = content.aux.lPrime + 1;

                    lowerChild = new SplittingTreeNode(0, this, splitResult.getDNF(),
                            splitResult.getOccurrences(), context,
                            SplittingNodeType::AUXILIARY_NODE, childContent);
                    /*new AuxiliaryNode(NULL, this, splitResult.getDNF(),
                            splitResult.getOccurrences(), context, lValue, lPrime + 1);*/
                }
                
                // symmetry test
                if (symmetryTest) {
                    // std::cout << "checking symmetry" << std::endl;
                    ClauseSet *existingDnf = upperChild->getDNF();
                    ClauseSet *testDnf = splitAway(0, v, false, true).getDNF();
                    if (*existingDnf != *testDnf) {
                        std::cout << *existingDnf << " and " << *testDnf <<
                            " are not symmetric" << std::endl;
                        assert(column > 0);
                        throw NotSymmetricException((*v)[column - 1], (*v)[column]);
                    }
                }
            }
            // std::cout << "END Split Aux " << this->upperChild << " " << this->lowerChild << std::endl;
        }

        /**
         * Return the \f$l\f$ value.
         *
         * Whenever a main node finds two or more symmetric variables
         * that are the most important ones it will calculate the maximal
         * \f$l\f$ value, again see
         * <a href="http://www.informatik.uni-freiburg.de/~ki/papers/smaus-tr230.pdf">
         * Smaus 2007
         *</a>. All auxiliary successors of the main node must know this value.
         *</a>.
         */
        size_t getL() const;

        /**
         * Get the \f$l'\f$ value.
         *
         * Each auxiliary node must know how many levels of
         * auxiliary nodes have been created. The node will use this value to
         * determine if it should again auxiliary successors or
         * main successors. I. e. auxiliary successors will be created until
         * there is an auxiliary node with \f$l' = l - 1\f$.
         *
         */
        size_t getLPrime() const;
        // end methods and fields for aux nodes

        SplittingNodeContent content;

        SplittingNodeContent &getContent();

        // TODO doc me
        // returns 0 if DNF is neither true nor false
        // 1 if it is false
        // 2 if it is true
        int isDNFTrueOrFalse(const ClauseSet &cs) const;
};

}

#endif  // SPLITTINGTREENODE_HPP_
